MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anim123i Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3anim123i.1 . . 3 (𝜑𝜓)
213ad2ant1 1132 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1133 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1134 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1127 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff setvar class
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 396  df-3an 1088
This theorem is referenced by:  3anim1i  1151  3anim2i  1152  3anim3i  1153  syl3an  1159  syl3anl  1414  eloprabga  7519  eloprabgaOLD  7520  le2tri3i  11349  fzmmmeqm  13539  elfz0fzfz0  13611  elfzmlbp  13617  elfzo1  13687  ssfzoulel  13731  flltdivnn0lt  13803  pfxeq  14651  swrdswrd  14660  swrdccat  14690  modmulconst  16236  nndvdslegcd  16451  ncoprmlnprm  16669  setsstruct2  17112  efmnd2hash  18812  symg2hash  19301  pmtrdifellem2  19387  unitgrp  20275  isdrngd  20534  isdrngdOLD  20536  bcthlem5  25077  lgsmulsqcoprm  27083  noetalem2  27482  colinearalg  28436  axcontlem8  28497  cplgr3v  28960  2wlkdlem3  29449  umgr2adedgwlk  29467  elwwlks2  29488  clwwlkinwwlk  29561  3wlkdlem5  29684  3wlkdlem6  29686  3wlkdlem7  29687  3wlkdlem8  29688  numclwwlk1lem2foalem  29872  chirredlem2  31912  rexdiv  32360  bnj944  34248  bnj969  34256  nnssi2  35644  nnssi3  35645  isdrngo2  37130  leatb  38466  paddasslem9  39003  paddasslem10  39004  dvhvaddass  40272  expgrowthi  43395  elsetpreimafveq  46364  nnsum4primesodd  46763  nnsum4primesoddALTV  46764  nn0mnd  46856  2zrngasgrp  46927  2zrngmsgrp  46934  mapprop  47111  lincvalpr  47187  refdivmptf  47316  refdivmptfv  47320  itsclc0yqsollem2  47537
  Copyright terms: Public domain W3C validator