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  7478  le2tri3i  11280  fzmmmeqm  13494  elfz0fzfz0  13570  elfzmlbp  13576  elfzo1  13649  ssfzoulel  13697  fvf1tp  13727  flltdivnn0lt  13771  hash7g  14427  pfxeq  14637  swrdswrd  14646  swrdccat  14676  modmulconst  16234  nndvdslegcd  16451  ncoprmlnprm  16674  setsstruct2  17120  efmnd2hash  18803  symg2hash  19306  pmtrdifellem2  19391  unitgrp  20303  isdrngd  20685  isdrngdOLD  20687  bcthlem5  25261  lgsmulsqcoprm  27287  noetalem2  27687  colinearalg  28890  axcontlem8  28951  cplgr3v  29415  2wlkdlem3  29907  umgr2adedgwlk  29925  elwwlks2  29946  clwwlkinwwlk  30019  3wlkdlem5  30142  3wlkdlem6  30144  3wlkdlem7  30145  3wlkdlem8  30146  numclwwlk1lem2foalem  30330  chirredlem2  32370  rexdiv  32896  bnj944  34921  bnj969  34929  nnssi2  36436  nnssi3  36437  isdrngo2  37945  leatb  39278  paddasslem9  39815  paddasslem10  39816  dvhvaddass  41084  expgrowthi  44315  elsetpreimafveq  47391  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  gpgusgralem  48040  nn0mnd  48160  2zrngasgrp  48227  2zrngmsgrp  48234  mapprop  48327  lincvalpr  48400  refdivmptf  48524  refdivmptfv  48528  itsclc0yqsollem2  48745