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  7470  le2tri3i  11270  fzmmmeqm  13505  elfz0fzfz0  13581  elfzmlbp  13587  elfzo1  13661  ssfzoulel  13709  fvf1tp  13742  flltdivnn0lt  13786  hash7g  14442  pfxeq  14652  swrdswrd  14661  swrdccat  14691  modmulconst  16251  nndvdslegcd  16468  ncoprmlnprm  16692  setsstruct2  17138  efmnd2hash  18856  symg2hash  19361  pmtrdifellem2  19446  unitgrp  20357  isdrngd  20736  isdrngdOLD  20738  bcthlem5  25308  lgsmulsqcoprm  27323  noetalem2  27723  colinearalg  28996  axcontlem8  29057  cplgr3v  29521  2wlkdlem3  30013  umgr2adedgwlk  30031  elwwlks2  30055  clwwlkinwwlk  30128  3wlkdlem5  30251  3wlkdlem6  30253  3wlkdlem7  30254  3wlkdlem8  30255  numclwwlk1lem2foalem  30439  chirredlem2  32480  rexdiv  33003  bnj944  35099  bnj969  35107  nnssi2  36656  nnssi3  36657  isdrngo2  38296  leatb  39755  paddasslem9  40291  paddasslem10  40292  dvhvaddass  41560  expgrowthi  44781  elsetpreimafveq  47872  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  gpgusgralem  48547  nn0mnd  48670  2zrngasgrp  48737  2zrngmsgrp  48744  mapprop  48837  lincvalpr  48909  refdivmptf  49033  refdivmptfv  49037  itsclc0yqsollem2  49254