Theorem 3anim123i 1150

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 1132	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1133	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1127	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3anim1i  1151  3anim2i  1152  3anim3i  1153  syl3an  1159  syl3anl  1414  eloprabga  7540  eloprabgaOLD  7541  le2tri3i  11388  fzmmmeqm  13593  elfz0fzfz0  13669  elfzmlbp  13675  elfzo1  13748  ssfzoulel  13795  fvf1tp  13825  flltdivnn0lt  13869  hash7g  14521  pfxeq  14730  swrdswrd  14739  swrdccat  14769  modmulconst  16321  nndvdslegcd  16538  ncoprmlnprm  16761  setsstruct2  17207  efmnd2hash  18919  symg2hash  19423  pmtrdifellem2  19509  unitgrp  20399  isdrngd  20781  isdrngdOLD  20783  bcthlem5  25375  lgsmulsqcoprm  27401  noetalem2  27801  colinearalg  28939  axcontlem8  29000  cplgr3v  29466  2wlkdlem3  29956  umgr2adedgwlk  29974  elwwlks2  29995  clwwlkinwwlk  30068  3wlkdlem5  30191  3wlkdlem6  30193  3wlkdlem7  30194  3wlkdlem8  30195  numclwwlk1lem2foalem  30379  chirredlem2  32419  rexdiv  32892  bnj944  34930  bnj969  34938  nnssi2  36437  nnssi3  36438  isdrngo2  37944  leatb  39273  paddasslem9  39810  paddasslem10  39811  dvhvaddass  41079  expgrowthi  44328  elsetpreimafveq  47321  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  gpgusgralem  47945  nn0mnd  48022  2zrngasgrp  48089  2zrngmsgrp  48096  mapprop  48190  lincvalpr  48263  refdivmptf  48391  refdivmptfv  48395  itsclc0yqsollem2  48612