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  7465  le2tri3i  11261  fzmmmeqm  13471  elfz0fzfz0  13547  elfzmlbp  13553  elfzo1  13626  ssfzoulel  13674  fvf1tp  13707  flltdivnn0lt  13751  hash7g  14407  pfxeq  14617  swrdswrd  14626  swrdccat  14656  modmulconst  16213  nndvdslegcd  16430  ncoprmlnprm  16653  setsstruct2  17099  efmnd2hash  18817  symg2hash  19319  pmtrdifellem2  19404  unitgrp  20317  isdrngd  20696  isdrngdOLD  20698  bcthlem5  25282  lgsmulsqcoprm  27308  noetalem2  27708  colinearalg  28932  axcontlem8  28993  cplgr3v  29457  2wlkdlem3  29949  umgr2adedgwlk  29967  elwwlks2  29991  clwwlkinwwlk  30064  3wlkdlem5  30187  3wlkdlem6  30189  3wlkdlem7  30190  3wlkdlem8  30191  numclwwlk1lem2foalem  30375  chirredlem2  32415  rexdiv  32956  bnj944  35043  bnj969  35051  nnssi2  36598  nnssi3  36599  isdrngo2  38098  leatb  39491  paddasslem9  40027  paddasslem10  40028  dvhvaddass  41296  expgrowthi  44516  elsetpreimafveq  47585  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  gpgusgralem  48244  nn0mnd  48367  2zrngasgrp  48434  2zrngmsgrp  48441  mapprop  48534  lincvalpr  48606  refdivmptf  48730  refdivmptfv  48734  itsclc0yqsollem2  48951