Theorem 3anim123i 1169

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 1151	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1152	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1153	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1146	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anim1i  1170  3anim2i  1171  3anim3i  1172  syl3an  1178  syl3anl  1442  eloprabga  7522  le2tri3i  11364  fzmmmeqm  13612  elfz0fzfz0  13688  elfzmlbp  13694  elfzo1  13768  ssfzoulel  13816  fvf1tp  13850  flltdivnn0lt  13894  hash7g  14551  pfxeq  14765  swrdswrd  14774  swrdccat  14804  modmulconst  16378  nndvdslegcd  16595  ncoprmlnprm  16819  setsstruct2  17266  efmnd2hash  19003  symg2hash  19519  pmtrdifellem2  19604  unitgrp  20524  isdrng3lem2  20915  isdrngd  20931  isdrngdOLD  20933  bcthlem5  25556  lgsmulsqcoprm  27579  noetalem2  27978  colinearalg  29367  axcontlem8  29428  cplgr3v  29895  2wlkdlem3  30395  umgr2adedgwlk  30413  elwwlks2  30437  clwwlkinwwlk  30510  3wlkdlem5  30643  3wlkdlem6  30645  3wlkdlem7  30646  3wlkdlem8  30647  numclwwlk1lem2foalem  30831  chirredlem2  32872  rexdiv  33371  bnj944  35447  bnj969  35455  wevonprcf1o  35710  nmulprop  36770  nnssi2  37074  nnssi3  37075  isdrngo2  38708  leatb  40165  paddasslem9  40701  paddasslem10  40702  dvhvaddass  41970  expgrowthi  45157  elsetpreimafveq  48297  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  gpgusgralem  48972  nn0mnd  49094  2zrngasgrp  49161  2zrngmsgrp  49168  mapprop  49276  lincvalpr  49348  refdivmptf  49472  refdivmptfv  49476  itsclc0yqsollem2  49693