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  1417  eloprabga  7542  le2tri3i  11391  fzmmmeqm  13597  elfz0fzfz0  13673  elfzmlbp  13679  elfzo1  13752  ssfzoulel  13799  fvf1tp  13829  flltdivnn0lt  13873  hash7g  14525  pfxeq  14734  swrdswrd  14743  swrdccat  14773  modmulconst  16325  nndvdslegcd  16542  ncoprmlnprm  16765  setsstruct2  17211  efmnd2hash  18907  symg2hash  19409  pmtrdifellem2  19495  unitgrp  20383  isdrngd  20765  isdrngdOLD  20767  bcthlem5  25362  lgsmulsqcoprm  27387  noetalem2  27787  colinearalg  28925  axcontlem8  28986  cplgr3v  29452  2wlkdlem3  29947  umgr2adedgwlk  29965  elwwlks2  29986  clwwlkinwwlk  30059  3wlkdlem5  30182  3wlkdlem6  30184  3wlkdlem7  30185  3wlkdlem8  30186  numclwwlk1lem2foalem  30370  chirredlem2  32410  rexdiv  32908  bnj944  34952  bnj969  34960  nnssi2  36456  nnssi3  36457  isdrngo2  37965  leatb  39293  paddasslem9  39830  paddasslem10  39831  dvhvaddass  41099  expgrowthi  44352  elsetpreimafveq  47384  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  gpgusgralem  48011  nn0mnd  48095  2zrngasgrp  48162  2zrngmsgrp  48169  mapprop  48262  lincvalpr  48335  refdivmptf  48463  refdivmptfv  48467  itsclc0yqsollem2  48684