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  7528  le2tri3i  11357  fzmmmeqm  13604  elfz0fzfz0  13680  elfzmlbp  13686  elfzo1  13760  ssfzoulel  13808  fvf1tp  13842  flltdivnn0lt  13886  hash7g  14543  pfxeq  14757  swrdswrd  14766  swrdccat  14796  modmulconst  16370  nndvdslegcd  16587  ncoprmlnprm  16811  setsstruct2  17258  efmnd2hash  18992  symg2hash  19508  pmtrdifellem2  19593  unitgrp  20513  isdrng3lem2  20904  isdrngd  20920  isdrngdOLD  20922  bcthlem5  25540  lgsmulsqcoprm  27560  noetalem2  27959  colinearalg  29317  axcontlem8  29378  cplgr3v  29845  2wlkdlem3  30345  umgr2adedgwlk  30363  elwwlks2  30387  clwwlkinwwlk  30460  3wlkdlem5  30587  3wlkdlem6  30589  3wlkdlem7  30590  3wlkdlem8  30591  numclwwlk1lem2foalem  30775  chirredlem2  32816  rexdiv  33317  bnj944  35393  bnj969  35401  wevonprcf1o  35656  nmulprop  36721  nnssi2  37025  nnssi3  37026  isdrngo2  38669  leatb  40126  paddasslem9  40662  paddasslem10  40663  dvhvaddass  41931  expgrowthi  45103  elsetpreimafveq  48206  nnsum4primesodd  48621  nnsum4primesoddALTV  48622  gpgusgralem  48881  nn0mnd  49003  2zrngasgrp  49070  2zrngmsgrp  49077  mapprop  49185  lincvalpr  49257  refdivmptf  49381  refdivmptfv  49385  itsclc0yqsollem2  49602