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 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anim1i  1170  3anim2i  1171  3anim3i  1172  syl3an  1178  syl3anl  1442  eloprabga  7519  le2tri3i  11335  fzmmmeqm  13581  elfz0fzfz0  13657  elfzmlbp  13663  elfzo1  13737  ssfzoulel  13785  fvf1tp  13818  flltdivnn0lt  13862  hash7g  14519  pfxeq  14729  swrdswrd  14738  swrdccat  14768  modmulconst  16341  nndvdslegcd  16558  ncoprmlnprm  16782  setsstruct2  17229  efmnd2hash  18948  symg2hash  19457  pmtrdifellem2  19542  unitgrp  20461  isdrng3lem2  20852  isdrngd  20868  isdrngdOLD  20870  bcthlem5  25487  lgsmulsqcoprm  27507  noetalem2  27906  colinearalg  29260  axcontlem8  29321  cplgr3v  29785  2wlkdlem3  30276  umgr2adedgwlk  30294  elwwlks2  30318  clwwlkinwwlk  30391  3wlkdlem5  30514  3wlkdlem6  30516  3wlkdlem7  30517  3wlkdlem8  30518  numclwwlk1lem2foalem  30702  chirredlem2  32743  rexdiv  33245  bnj944  35326  bnj969  35334  wevonprcf1o  35597  nmulprop  36682  nnssi2  36986  nnssi3  36987  isdrngo2  38629  leatb  40086  paddasslem9  40622  paddasslem10  40623  dvhvaddass  41891  expgrowthi  45063  elsetpreimafveq  48166  nnsum4primesodd  48581  nnsum4primesoddALTV  48582  gpgusgralem  48841  nn0mnd  48964  2zrngasgrp  49031  2zrngmsgrp  49038  mapprop  49146  lincvalpr  49218  refdivmptf  49342  refdivmptfv  49346  itsclc0yqsollem2  49563