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 1087

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 1089

This theorem is referenced by:  3anim1i  1152  3anim2i  1153  3anim3i  1154  syl3an  1160  syl3anl  1415  eloprabga  7558  eloprabgaOLD  7559  le2tri3i  11420  fzmmmeqm  13617  elfz0fzfz0  13690  elfzmlbp  13696  elfzo1  13766  ssfzoulel  13810  fvf1tp  13840  flltdivnn0lt  13884  hash7g  14535  pfxeq  14744  swrdswrd  14753  swrdccat  14783  modmulconst  16336  nndvdslegcd  16551  ncoprmlnprm  16775  setsstruct2  17221  efmnd2hash  18929  symg2hash  19433  pmtrdifellem2  19519  unitgrp  20409  isdrngd  20787  isdrngdOLD  20789  bcthlem5  25381  lgsmulsqcoprm  27405  noetalem2  27805  colinearalg  28943  axcontlem8  29004  cplgr3v  29470  2wlkdlem3  29960  umgr2adedgwlk  29978  elwwlks2  29999  clwwlkinwwlk  30072  3wlkdlem5  30195  3wlkdlem6  30197  3wlkdlem7  30198  3wlkdlem8  30199  numclwwlk1lem2foalem  30383  chirredlem2  32423  rexdiv  32890  bnj944  34914  bnj969  34922  nnssi2  36421  nnssi3  36422  isdrngo2  37918  leatb  39248  paddasslem9  39785  paddasslem10  39786  dvhvaddass  41054  expgrowthi  44302  elsetpreimafveq  47271  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nn0mnd  47902  2zrngasgrp  47969  2zrngmsgrp  47976  mapprop  48071  lincvalpr  48147  refdivmptf  48276  refdivmptfv  48280  itsclc0yqsollem2  48497