Theorem 3anim123i 1157

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 1139	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓)
3		3anim123i.2	. . 3 ⊢ (𝜒 → 𝜃)
4	3	3ad2ant2 1140	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃)
5		3anim123i.3	. . 3 ⊢ (𝜏 → 𝜂)
6	5	3ad2ant3 1141	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
7	2, 4, 6	3jca 1134	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anim1i  1158  3anim2i  1159  3anim3i  1160  syl3an  1166  syl3anl  1423  eloprabga  7465  le2tri3i  11267  fzmmmeqm  13502  elfz0fzfz0  13578  elfzmlbp  13584  elfzo1  13658  ssfzoulel  13706  fvf1tp  13739  flltdivnn0lt  13783  hash7g  14439  pfxeq  14649  swrdswrd  14658  swrdccat  14688  modmulconst  16248  nndvdslegcd  16465  ncoprmlnprm  16689  setsstruct2  17135  efmnd2hash  18853  symg2hash  19358  pmtrdifellem2  19443  unitgrp  20354  isdrngd  20737  isdrngdOLD  20739  bcthlem5  25313  lgsmulsqcoprm  27324  noetalem2  27724  colinearalg  28997  axcontlem8  29058  cplgr3v  29522  2wlkdlem3  30013  umgr2adedgwlk  30031  elwwlks2  30055  clwwlkinwwlk  30128  3wlkdlem5  30251  3wlkdlem6  30253  3wlkdlem7  30254  3wlkdlem8  30255  numclwwlk1lem2foalem  30439  chirredlem2  32480  rexdiv  33004  bnj944  35120  bnj969  35128  nnssi2  36683  nnssi3  36684  isdrngo2  38325  leatb  39784  paddasslem9  40320  paddasslem10  40321  dvhvaddass  41589  expgrowthi  44777  elsetpreimafveq  47872  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  gpgusgralem  48547  nn0mnd  48670  2zrngasgrp  48737  2zrngmsgrp  48744  mapprop  48837  lincvalpr  48909  refdivmptf  49033  refdivmptfv  49037  itsclc0yqsollem2  49254