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  7529  le2tri3i  11440  fzmmmeqm  13691  elfz0fzfz0  13767  elfzmlbp  13773  elfzo1  13847  ssfzoulel  13895  fvf1tp  13929  flltdivnn0lt  13973  hash7g  14631  pfxeq  14845  swrdswrd  14854  swrdccat  14884  modmulconst  16458  nndvdslegcd  16675  ncoprmlnprm  16904  setsstruct2  17352  efmnd2hash  19090  symg2hash  19606  pmtrdifellem2  19691  unitgrp  20613  isdrng3lem2  21006  isdrngd  21022  isdrngdOLD  21024  bcthlem5  25649  lgsmulsqcoprm  27670  noetalem2  28099  colinearalg  29488  axcontlem8  29549  cplgr3v  30016  2wlkdlem3  30516  umgr2adedgwlk  30534  elwwlks2  30558  clwwlkinwwlk  30631  3wlkdlem5  30764  3wlkdlem6  30766  3wlkdlem7  30767  3wlkdlem8  30768  numclwwlk1lem2foalem  30952  chirredlem2  32993  rexdiv  33492  bnj944  35568  bnj969  35576  wevonprcf1o  35892  nmulprop  36939  nnssi2  37243  nnssi3  37244  isdrngo2  38892  leatb  40349  paddasslem9  40885  paddasslem10  40886  dvhvaddass  42154  expgrowthi  45316  elsetpreimafveq  48478  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  gpgusgralem  49153  nn0mnd  49275  2zrngasgrp  49342  2zrngmsgrp  49349  mapprop  49457  lincvalpr  49529  refdivmptf  49653  refdivmptfv  49657  itsclc0yqsollem2  49874