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  7467  le2tri3i  11263  fzmmmeqm  13473  elfz0fzfz0  13549  elfzmlbp  13555  elfzo1  13628  ssfzoulel  13676  fvf1tp  13709  flltdivnn0lt  13753  hash7g  14409  pfxeq  14619  swrdswrd  14628  swrdccat  14658  modmulconst  16215  nndvdslegcd  16432  ncoprmlnprm  16655  setsstruct2  17101  efmnd2hash  18819  symg2hash  19321  pmtrdifellem2  19406  unitgrp  20319  isdrngd  20698  isdrngdOLD  20700  bcthlem5  25284  lgsmulsqcoprm  27310  noetalem2  27710  colinearalg  28983  axcontlem8  29044  cplgr3v  29508  2wlkdlem3  30000  umgr2adedgwlk  30018  elwwlks2  30042  clwwlkinwwlk  30115  3wlkdlem5  30238  3wlkdlem6  30240  3wlkdlem7  30241  3wlkdlem8  30242  numclwwlk1lem2foalem  30426  chirredlem2  32466  rexdiv  33007  bnj944  35094  bnj969  35102  nnssi2  36649  nnssi3  36650  isdrngo2  38159  leatb  39562  paddasslem9  40098  paddasslem10  40099  dvhvaddass  41367  expgrowthi  44584  elsetpreimafveq  47653  nnsum4primesodd  48052  nnsum4primesoddALTV  48053  gpgusgralem  48312  nn0mnd  48435  2zrngasgrp  48502  2zrngmsgrp  48509  mapprop  48602  lincvalpr  48674  refdivmptf  48798  refdivmptfv  48802  itsclc0yqsollem2  49019