Theorem 3anim123i 1147

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 1129	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1130	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1131	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1124	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3anim1i  1148  3anim2i  1149  3anim3i  1150  syl3an  1156  syl3anl  1411  eloprabga  7264  le2tri3i  10773  fzmmmeqm  12943  elfz0fzfz0  13015  elfzmlbp  13021  elfzo1  13090  ssfzoulel  13134  flltdivnn0lt  13206  pfxeq  14061  swrdswrd  14070  swrdccat  14100  modmulconst  15644  nndvdslegcd  15857  ncoprmlnprm  16071  setsstruct2  16524  efmnd2hash  18062  symg2hash  18523  pmtrdifellem2  18608  unitgrp  19420  isdrngd  19530  bcthlem5  23934  lgsmulsqcoprm  25922  colinearalg  26699  axcontlem8  26760  cplgr3v  27220  2wlkdlem3  27709  umgr2adedgwlk  27727  elwwlks2  27748  clwwlkinwwlk  27821  3wlkdlem5  27945  3wlkdlem6  27947  3wlkdlem7  27948  3wlkdlem8  27949  numclwwlk1lem2foalem  28133  chirredlem2  30171  rexdiv  30606  bnj944  32214  bnj969  32222  nnssi2  33807  nnssi3  33808  isdrngo2  35240  leatb  36432  paddasslem9  36968  paddasslem10  36969  dvhvaddass  38237  expgrowthi  40671  elsetpreimafveq  43564  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  nn0mnd  44093  2zrngasgrp  44218  2zrngmsgrp  44225  lincvalpr  44480  refdivmptf  44609  refdivmptfv  44613  itsclc0yqsollem2  44757