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  7501  le2tri3i  11311  fzmmmeqm  13525  elfz0fzfz0  13601  elfzmlbp  13607  elfzo1  13680  ssfzoulel  13728  fvf1tp  13758  flltdivnn0lt  13802  hash7g  14458  pfxeq  14668  swrdswrd  14677  swrdccat  14707  modmulconst  16265  nndvdslegcd  16482  ncoprmlnprm  16705  setsstruct2  17151  efmnd2hash  18828  symg2hash  19329  pmtrdifellem2  19414  unitgrp  20299  isdrngd  20681  isdrngdOLD  20683  bcthlem5  25235  lgsmulsqcoprm  27261  noetalem2  27661  colinearalg  28844  axcontlem8  28905  cplgr3v  29369  2wlkdlem3  29864  umgr2adedgwlk  29882  elwwlks2  29903  clwwlkinwwlk  29976  3wlkdlem5  30099  3wlkdlem6  30101  3wlkdlem7  30102  3wlkdlem8  30103  numclwwlk1lem2foalem  30287  chirredlem2  32327  rexdiv  32853  bnj944  34935  bnj969  34943  nnssi2  36450  nnssi3  36451  isdrngo2  37959  leatb  39292  paddasslem9  39829  paddasslem10  39830  dvhvaddass  41098  expgrowthi  44329  elsetpreimafveq  47402  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  gpgusgralem  48051  nn0mnd  48171  2zrngasgrp  48238  2zrngmsgrp  48245  mapprop  48338  lincvalpr  48411  refdivmptf  48535  refdivmptfv  48539  itsclc0yqsollem2  48756