Theorem 3anim123i 1152

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 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1135	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1136	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1129	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anim1i  1153  3anim2i  1154  3anim3i  1155  syl3an  1161  syl3anl  1418  eloprabga  7476  le2tri3i  11276  fzmmmeqm  13511  elfz0fzfz0  13587  elfzmlbp  13593  elfzo1  13667  ssfzoulel  13715  fvf1tp  13748  flltdivnn0lt  13792  hash7g  14448  pfxeq  14658  swrdswrd  14667  swrdccat  14697  modmulconst  16257  nndvdslegcd  16474  ncoprmlnprm  16698  setsstruct2  17144  efmnd2hash  18862  symg2hash  19367  pmtrdifellem2  19452  unitgrp  20363  isdrngd  20742  isdrngdOLD  20744  bcthlem5  25295  lgsmulsqcoprm  27306  noetalem2  27706  colinearalg  28979  axcontlem8  29040  cplgr3v  29504  2wlkdlem3  29995  umgr2adedgwlk  30013  elwwlks2  30037  clwwlkinwwlk  30110  3wlkdlem5  30233  3wlkdlem6  30235  3wlkdlem7  30236  3wlkdlem8  30237  numclwwlk1lem2foalem  30421  chirredlem2  32462  rexdiv  32985  bnj944  35080  bnj969  35088  nnssi2  36637  nnssi3  36638  isdrngo2  38279  leatb  39738  paddasslem9  40274  paddasslem10  40275  dvhvaddass  41543  expgrowthi  44760  elsetpreimafveq  47857  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  gpgusgralem  48532  nn0mnd  48655  2zrngasgrp  48722  2zrngmsgrp  48729  mapprop  48822  lincvalpr  48894  refdivmptf  49018  refdivmptfv  49022  itsclc0yqsollem2  49239