Theorem 3anim123i 1151

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 1133	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1135	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1128	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  1152  3anim2i  1153  3anim3i  1154  syl3an  1160  syl3anl  1417  eloprabga  7516  le2tri3i  11365  fzmmmeqm  13574  elfz0fzfz0  13650  elfzmlbp  13656  elfzo1  13729  ssfzoulel  13776  fvf1tp  13806  flltdivnn0lt  13850  hash7g  14504  pfxeq  14714  swrdswrd  14723  swrdccat  14753  modmulconst  16307  nndvdslegcd  16524  ncoprmlnprm  16747  setsstruct2  17193  efmnd2hash  18872  symg2hash  19373  pmtrdifellem2  19458  unitgrp  20343  isdrngd  20725  isdrngdOLD  20727  bcthlem5  25280  lgsmulsqcoprm  27306  noetalem2  27706  colinearalg  28889  axcontlem8  28950  cplgr3v  29414  2wlkdlem3  29909  umgr2adedgwlk  29927  elwwlks2  29948  clwwlkinwwlk  30021  3wlkdlem5  30144  3wlkdlem6  30146  3wlkdlem7  30147  3wlkdlem8  30148  numclwwlk1lem2foalem  30332  chirredlem2  32372  rexdiv  32900  bnj944  34969  bnj969  34977  nnssi2  36473  nnssi3  36474  isdrngo2  37982  leatb  39310  paddasslem9  39847  paddasslem10  39848  dvhvaddass  41116  expgrowthi  44357  elsetpreimafveq  47411  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  gpgusgralem  48060  nn0mnd  48154  2zrngasgrp  48221  2zrngmsgrp  48228  mapprop  48321  lincvalpr  48394  refdivmptf  48522  refdivmptfv  48526  itsclc0yqsollem2  48743