Theorem 3anim123i 1150

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 1132	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1133	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1127	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  3anim1i  1151  3anim2i  1152  3anim3i  1153  syl3an  1159  syl3anl  1414  eloprabga  7519  eloprabgaOLD  7520  le2tri3i  11349  fzmmmeqm  13539  elfz0fzfz0  13611  elfzmlbp  13617  elfzo1  13687  ssfzoulel  13731  flltdivnn0lt  13803  pfxeq  14651  swrdswrd  14660  swrdccat  14690  modmulconst  16236  nndvdslegcd  16451  ncoprmlnprm  16669  setsstruct2  17112  efmnd2hash  18812  symg2hash  19301  pmtrdifellem2  19387  unitgrp  20275  isdrngd  20534  isdrngdOLD  20536  bcthlem5  25077  lgsmulsqcoprm  27083  noetalem2  27482  colinearalg  28436  axcontlem8  28497  cplgr3v  28960  2wlkdlem3  29449  umgr2adedgwlk  29467  elwwlks2  29488  clwwlkinwwlk  29561  3wlkdlem5  29684  3wlkdlem6  29686  3wlkdlem7  29687  3wlkdlem8  29688  numclwwlk1lem2foalem  29872  chirredlem2  31912  rexdiv  32360  bnj944  34248  bnj969  34256  nnssi2  35644  nnssi3  35645  isdrngo2  37130  leatb  38466  paddasslem9  39003  paddasslem10  39004  dvhvaddass  40272  expgrowthi  43395  elsetpreimafveq  46364  nnsum4primesodd  46763  nnsum4primesoddALTV  46764  nn0mnd  46856  2zrngasgrp  46927  2zrngmsgrp  46934  mapprop  47111  lincvalpr  47187  refdivmptf  47316  refdivmptfv  47320  itsclc0yqsollem2  47537