Theorem 3anim123i 1247

Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)

Hypotheses

Ref	Expression
3anim123i.1	⊢ (𝜑 → 𝜓)
3anim123i.2	⊢ (𝜒 → 𝜃)
3anim123i.3	⊢ (𝜏 → 𝜂)

Assertion

Ref	Expression
3anim123i	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Proof of Theorem 3anim123i

Step	Hyp	Ref	Expression
1		3anim123i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3ad2ant1 1082	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1083	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1084	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1242	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anim1i  1248  3anim2i  1249  3anim3i  1250  syl3an  1368  syl3anl  1377  spc3egv  3297  eloprabga  6747  le2tri3i  10167  fzmmmeqm  12374  elfz0fzfz0  12444  elfzmlbp  12450  elfzo1  12517  ssfzoulel  12562  flltdivnn0lt  12634  swrdswrd  13460  swrdccatin2  13487  swrdccat  13493  modmulconst  15013  mulmoddvds  15051  nndvdslegcd  15227  ncoprmlnprm  15436  setsstruct2  15896  symg2hash  17817  pmtrdifellem2  17897  unitgrp  18667  isdrngd  18772  bcthlem5  23125  lgsmulsqcoprm  25068  colinearalg  25790  axcontlem8  25851  cplgr3v  26331  2wlkdlem3  26823  umgr2adedgwlk  26841  elwwlks2  26861  clwwlkinwwlk  26905  3wlkdlem5  27023  3wlkdlem6  27025  3wlkdlem7  27026  3wlkdlem8  27027  numclwlk1lem2foalem  27222  chirredlem2  29250  rexdiv  29634  bnj944  31008  bnj969  31016  nnssi2  32454  nnssi3  32455  isdrngo2  33757  leatb  34579  paddasslem9  35114  paddasslem10  35115  dvhvaddass  36386  expgrowthi  38532  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  2zrngasgrp  41940  2zrngmsgrp  41947  lincvalpr  42207  refdivmptf  42336  refdivmptfv  42340