Theorem 3anim123i 1169

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anim1i  1170  3anim2i  1171  3anim3i  1172  syl3an  1178  syl3anl  1442  eloprabga  7536  le2tri3i  11450  fzmmmeqm  13701  elfz0fzfz0  13777  elfzmlbp  13783  elfzo1  13857  ssfzoulel  13905  fvf1tp  13939  flltdivnn0lt  13983  hash7g  14641  pfxeq  14856  swrdswrd  14865  swrdccat  14895  modmulconst  16470  nndvdslegcd  16687  ncoprmlnprm  16916  setsstruct2  17364  efmnd2hash  19102  symg2hash  19618  pmtrdifellem2  19703  unitgrp  20625  isdrng3lem2  21018  isdrngd  21034  isdrngdOLD  21036  bcthlem5  25661  lgsmulsqcoprm  27682  noetalem2  28111  colinearalg  29500  axcontlem8  29561  cplgr3v  30028  2wlkdlem3  30528  umgr2adedgwlk  30546  elwwlks2  30570  clwwlkinwwlk  30643  3wlkdlem5  30776  3wlkdlem6  30778  3wlkdlem7  30779  3wlkdlem8  30780  numclwwlk1lem2foalem  30964  chirredlem2  33005  rexdiv  33545  bnj944  35621  bnj969  35629  wevonprcf1o  35996  nmulprop  37066  nnssi2  37370  nnssi3  37371  isdrngo2  39032  leatb  40489  paddasslem9  41025  paddasslem10  41026  dvhvaddass  42294  expgrowthi  45457  elsetpreimafveq  48618  nnsum4primesodd  49033  nnsum4primesoddALTV  49034  gpgusgralem  49293  nn0mnd  49415  2zrngasgrp  49482  2zrngmsgrp  49489  mapprop  49597  lincvalpr  49669  refdivmptf  49793  refdivmptfv  49797  itsclc0yqsollem2  50014