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  7455  le2tri3i  11243  fzmmmeqm  13457  elfz0fzfz0  13533  elfzmlbp  13539  elfzo1  13612  ssfzoulel  13660  fvf1tp  13693  flltdivnn0lt  13737  hash7g  14393  pfxeq  14603  swrdswrd  14612  swrdccat  14642  modmulconst  16199  nndvdslegcd  16416  ncoprmlnprm  16639  setsstruct2  17085  efmnd2hash  18802  symg2hash  19304  pmtrdifellem2  19389  unitgrp  20301  isdrngd  20680  isdrngdOLD  20682  bcthlem5  25255  lgsmulsqcoprm  27281  noetalem2  27681  colinearalg  28888  axcontlem8  28949  cplgr3v  29413  2wlkdlem3  29905  umgr2adedgwlk  29923  elwwlks2  29947  clwwlkinwwlk  30020  3wlkdlem5  30143  3wlkdlem6  30145  3wlkdlem7  30146  3wlkdlem8  30147  numclwwlk1lem2foalem  30331  chirredlem2  32371  rexdiv  32906  bnj944  34950  bnj969  34958  nnssi2  36499  nnssi3  36500  isdrngo2  38008  leatb  39401  paddasslem9  39937  paddasslem10  39938  dvhvaddass  41206  expgrowthi  44436  elsetpreimafveq  47507  nnsum4primesodd  47906  nnsum4primesoddALTV  47907  gpgusgralem  48166  nn0mnd  48289  2zrngasgrp  48356  2zrngmsgrp  48363  mapprop  48456  lincvalpr  48529  refdivmptf  48653  refdivmptfv  48657  itsclc0yqsollem2  48874