Theorem 3anim123i 1151

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3anim1i  1152  3anim2i  1153  3anim3i  1154  syl3an  1160  syl3anl  1417  eloprabga  7458  le2tri3i  11246  fzmmmeqm  13460  elfz0fzfz0  13536  elfzmlbp  13542  elfzo1  13615  ssfzoulel  13663  fvf1tp  13693  flltdivnn0lt  13737  hash7g  14393  pfxeq  14602  swrdswrd  14611  swrdccat  14641  modmulconst  16199  nndvdslegcd  16416  ncoprmlnprm  16639  setsstruct2  17085  efmnd2hash  18768  symg2hash  19271  pmtrdifellem2  19356  unitgrp  20268  isdrngd  20650  isdrngdOLD  20652  bcthlem5  25226  lgsmulsqcoprm  27252  noetalem2  27652  colinearalg  28855  axcontlem8  28916  cplgr3v  29380  2wlkdlem3  29872  umgr2adedgwlk  29890  elwwlks2  29911  clwwlkinwwlk  29984  3wlkdlem5  30107  3wlkdlem6  30109  3wlkdlem7  30110  3wlkdlem8  30111  numclwwlk1lem2foalem  30295  chirredlem2  32335  rexdiv  32867  bnj944  34911  bnj969  34919  nnssi2  36439  nnssi3  36440  isdrngo2  37948  leatb  39281  paddasslem9  39817  paddasslem10  39818  dvhvaddass  41086  expgrowthi  44316  elsetpreimafveq  47391  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  gpgusgralem  48050  nn0mnd  48173  2zrngasgrp  48240  2zrngmsgrp  48247  mapprop  48340  lincvalpr  48413  refdivmptf  48537  refdivmptfv  48541  itsclc0yqsollem2  48758