Theorem 3anim123i 1149

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3anim1i  1150  3anim2i  1151  3anim3i  1152  syl3an  1158  syl3anl  1413  eloprabga  7360  eloprabgaOLD  7361  le2tri3i  11035  fzmmmeqm  13218  elfz0fzfz0  13290  elfzmlbp  13296  elfzo1  13365  ssfzoulel  13409  flltdivnn0lt  13481  pfxeq  14337  swrdswrd  14346  swrdccat  14376  modmulconst  15925  nndvdslegcd  16140  ncoprmlnprm  16360  setsstruct2  16803  efmnd2hash  18448  symg2hash  18914  pmtrdifellem2  19000  unitgrp  19824  isdrngd  19931  bcthlem5  24397  lgsmulsqcoprm  26396  colinearalg  27181  axcontlem8  27242  cplgr3v  27705  2wlkdlem3  28193  umgr2adedgwlk  28211  elwwlks2  28232  clwwlkinwwlk  28305  3wlkdlem5  28428  3wlkdlem6  28430  3wlkdlem7  28431  3wlkdlem8  28432  numclwwlk1lem2foalem  28616  chirredlem2  30654  rexdiv  31102  bnj944  32818  bnj969  32826  noetalem2  33872  nnssi2  34571  nnssi3  34572  isdrngo2  36043  leatb  37233  paddasslem9  37769  paddasslem10  37770  dvhvaddass  39038  expgrowthi  41840  elsetpreimafveq  44737  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nn0mnd  45261  2zrngasgrp  45386  2zrngmsgrp  45393  mapprop  45570  lincvalpr  45647  refdivmptf  45776  refdivmptfv  45780  itsclc0yqsollem2  45997