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  7255  le2tri3i  10764  fzmmmeqm  12934  elfz0fzfz0  13006  elfzmlbp  13012  elfzo1  13081  ssfzoulel  13125  flltdivnn0lt  13197  pfxeq  14052  swrdswrd  14061  swrdccat  14091  modmulconst  15635  nndvdslegcd  15848  ncoprmlnprm  16062  setsstruct2  16515  efmnd2hash  18053  symg2hash  18514  pmtrdifellem2  18599  unitgrp  19411  isdrngd  19521  bcthlem5  23925  lgsmulsqcoprm  25913  colinearalg  26690  axcontlem8  26751  cplgr3v  27211  2wlkdlem3  27700  umgr2adedgwlk  27718  elwwlks2  27739  clwwlkinwwlk  27812  3wlkdlem5  27936  3wlkdlem6  27938  3wlkdlem7  27939  3wlkdlem8  27940  numclwwlk1lem2foalem  28124  chirredlem2  30162  rexdiv  30597  bnj944  32205  bnj969  32213  nnssi2  33798  nnssi3  33799  isdrngo2  35230  leatb  36422  paddasslem9  36958  paddasslem10  36959  dvhvaddass  38227  expgrowthi  40658  elsetpreimafveq  43551  nnsum4primesodd  43955  nnsum4primesoddALTV  43956  nn0mnd  44080  2zrngasgrp  44205  2zrngmsgrp  44212  lincvalpr  44467  refdivmptf  44596  refdivmptfv  44600  itsclc0yqsollem2  44744