Theorem 3anim123i 1152

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 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1135	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1136	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1129	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  1153  3anim2i  1154  3anim3i  1155  syl3an  1161  syl3anl  1418  eloprabga  7477  le2tri3i  11275  fzmmmeqm  13485  elfz0fzfz0  13561  elfzmlbp  13567  elfzo1  13640  ssfzoulel  13688  fvf1tp  13721  flltdivnn0lt  13765  hash7g  14421  pfxeq  14631  swrdswrd  14640  swrdccat  14670  modmulconst  16227  nndvdslegcd  16444  ncoprmlnprm  16667  setsstruct2  17113  efmnd2hash  18831  symg2hash  19336  pmtrdifellem2  19421  unitgrp  20334  isdrngd  20713  isdrngdOLD  20715  bcthlem5  25299  lgsmulsqcoprm  27325  noetalem2  27725  colinearalg  28999  axcontlem8  29060  cplgr3v  29524  2wlkdlem3  30016  umgr2adedgwlk  30034  elwwlks2  30058  clwwlkinwwlk  30131  3wlkdlem5  30254  3wlkdlem6  30256  3wlkdlem7  30257  3wlkdlem8  30258  numclwwlk1lem2foalem  30442  chirredlem2  32483  rexdiv  33022  bnj944  35118  bnj969  35126  nnssi2  36675  nnssi3  36676  isdrngo2  38213  leatb  39672  paddasslem9  40208  paddasslem10  40209  dvhvaddass  41477  expgrowthi  44693  elsetpreimafveq  47761  nnsum4primesodd  48160  nnsum4primesoddALTV  48161  gpgusgralem  48420  nn0mnd  48543  2zrngasgrp  48610  2zrngmsgrp  48617  mapprop  48710  lincvalpr  48782  refdivmptf  48906  refdivmptfv  48910  itsclc0yqsollem2  49127