Theorem 3anim123i 1164

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 1146	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1147	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1148	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1141	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1098

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 400  df-3an 1100

This theorem is referenced by:  3anim1i  1165  3anim2i  1166  3anim3i  1167  syl3an  1173  syl3anl  1434  eloprabga  7505  le2tri3i  11313  fzmmmeqm  13562  elfz0fzfz0  13638  elfzmlbp  13644  elfzo1  13718  ssfzoulel  13766  fvf1tp  13799  flltdivnn0lt  13843  hash7g  14499  pfxeq  14709  swrdswrd  14718  swrdccat  14748  modmulconst  16322  nndvdslegcd  16539  ncoprmlnprm  16763  setsstruct2  17210  efmnd2hash  18928  symg2hash  19432  pmtrdifellem2  19517  unitgrp  20432  isdrngd  20815  isdrngdOLD  20817  bcthlem5  25390  lgsmulsqcoprm  27407  noetalem2  27806  colinearalg  29111  axcontlem8  29172  cplgr3v  29636  2wlkdlem3  30127  umgr2adedgwlk  30145  elwwlks2  30169  clwwlkinwwlk  30242  3wlkdlem5  30365  3wlkdlem6  30367  3wlkdlem7  30368  3wlkdlem8  30369  numclwwlk1lem2foalem  30553  chirredlem2  32594  rexdiv  33103  bnj944  35233  bnj969  35241  wevonprcf1o  35456  nmulprop  36540  nnssi2  36815  nnssi3  36816  isdrngo2  38457  leatb  39916  paddasslem9  40452  paddasslem10  40453  dvhvaddass  41721  expgrowthi  44909  elsetpreimafveq  48003  nnsum4primesodd  48418  nnsum4primesoddALTV  48419  gpgusgralem  48678  nn0mnd  48801  2zrngasgrp  48868  2zrngmsgrp  48875  mapprop  48968  lincvalpr  49040  refdivmptf  49164  refdivmptfv  49168  itsclc0yqsollem2  49385