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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anim1i  1170  3anim2i  1171  3anim3i  1172  syl3an  1178  syl3anl  1443  eloprabga  7560  le2tri3i  11479  fzmmmeqm  13731  elfz0fzfz0  13807  elfzmlbp  13813  elfzo1  13887  ssfzoulel  13935  fvf1tp  13969  flltdivnn0lt  14013  hash7g  14672  pfxeq  14887  swrdswrd  14896  swrdccat  14926  modmulconst  16502  nndvdslegcd  16719  ncoprmlnprm  16948  setsstruct2  17396  efmnd2hash  19140  symg2hash  19657  pmtrdifellem2  19742  unitgrp  20664  isdrng3lem2  21057  isdrngd  21073  isdrngdOLD  21075  bcthlem5  25704  lgsmulsqcoprm  27727  noetalem2  28156  colinearalg  29545  axcontlem8  29606  cplgr3v  30073  2wlkdlem3  30573  umgr2adedgwlk  30591  elwwlks2  30615  clwwlkinwwlk  30688  3wlkdlem5  30821  3wlkdlem6  30823  3wlkdlem7  30824  3wlkdlem8  30825  numclwwlk1lem2foalem  31009  chirredlem2  33050  rexdiv  33588  bnj944  35679  bnj969  35687  wevonprcf1o  36083  nmulprop  37154  nnssi2  37458  nnssi3  37459  isdrngo2  39158  leatb  40615  paddasslem9  41151  paddasslem10  41152  dvhvaddass  42420  expgrowthi  45578  elsetpreimafveq  48752  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  gpgusgralem  49427  nn0mnd  49549  2zrngasgrp  49616  2zrngmsgrp  49623  mapprop  49789  lincvalpr  49861  refdivmptf  49985  refdivmptfv  49989  itsclc0yqsollem2  50206