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  7498  le2tri3i  11304  fzmmmeqm  13518  elfz0fzfz0  13594  elfzmlbp  13600  elfzo1  13673  ssfzoulel  13721  fvf1tp  13751  flltdivnn0lt  13795  hash7g  14451  pfxeq  14661  swrdswrd  14670  swrdccat  14700  modmulconst  16258  nndvdslegcd  16475  ncoprmlnprm  16698  setsstruct2  17144  efmnd2hash  18821  symg2hash  19322  pmtrdifellem2  19407  unitgrp  20292  isdrngd  20674  isdrngdOLD  20676  bcthlem5  25228  lgsmulsqcoprm  27254  noetalem2  27654  colinearalg  28837  axcontlem8  28898  cplgr3v  29362  2wlkdlem3  29857  umgr2adedgwlk  29875  elwwlks2  29896  clwwlkinwwlk  29969  3wlkdlem5  30092  3wlkdlem6  30094  3wlkdlem7  30095  3wlkdlem8  30096  numclwwlk1lem2foalem  30280  chirredlem2  32320  rexdiv  32846  bnj944  34928  bnj969  34936  nnssi2  36443  nnssi3  36444  isdrngo2  37952  leatb  39285  paddasslem9  39822  paddasslem10  39823  dvhvaddass  41091  expgrowthi  44322  elsetpreimafveq  47398  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  gpgusgralem  48047  nn0mnd  48167  2zrngasgrp  48234  2zrngmsgrp  48241  mapprop  48334  lincvalpr  48407  refdivmptf  48531  refdivmptfv  48535  itsclc0yqsollem2  48752