Theorem 3anim123i 1150

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 1132	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1133	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1127	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anim1i  1151  3anim2i  1152  3anim3i  1153  syl3an  1159  syl3anl  1414  eloprabga  7382  eloprabgaOLD  7383  le2tri3i  11105  fzmmmeqm  13289  elfz0fzfz0  13361  elfzmlbp  13367  elfzo1  13437  ssfzoulel  13481  flltdivnn0lt  13553  pfxeq  14409  swrdswrd  14418  swrdccat  14448  modmulconst  15997  nndvdslegcd  16212  ncoprmlnprm  16432  setsstruct2  16875  efmnd2hash  18533  symg2hash  18999  pmtrdifellem2  19085  unitgrp  19909  isdrngd  20016  bcthlem5  24492  lgsmulsqcoprm  26491  colinearalg  27278  axcontlem8  27339  cplgr3v  27802  2wlkdlem3  28292  umgr2adedgwlk  28310  elwwlks2  28331  clwwlkinwwlk  28404  3wlkdlem5  28527  3wlkdlem6  28529  3wlkdlem7  28530  3wlkdlem8  28531  numclwwlk1lem2foalem  28715  chirredlem2  30753  rexdiv  31200  bnj944  32918  bnj969  32926  noetalem2  33945  nnssi2  34644  nnssi3  34645  isdrngo2  36116  leatb  37306  paddasslem9  37842  paddasslem10  37843  dvhvaddass  39111  expgrowthi  41951  elsetpreimafveq  44849  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  nn0mnd  45373  2zrngasgrp  45498  2zrngmsgrp  45505  mapprop  45682  lincvalpr  45759  refdivmptf  45888  refdivmptfv  45892  itsclc0yqsollem2  46109