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

Theorem 3anim123i 1152
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 1134 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1135 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1136 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1129 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 1089
This theorem is referenced by:  3anim1i  1153  3anim2i  1154  3anim3i  1155  syl3an  1161  syl3anl  1417  eloprabga  7542  le2tri3i  11391  fzmmmeqm  13597  elfz0fzfz0  13673  elfzmlbp  13679  elfzo1  13752  ssfzoulel  13799  fvf1tp  13829  flltdivnn0lt  13873  hash7g  14525  pfxeq  14734  swrdswrd  14743  swrdccat  14773  modmulconst  16325  nndvdslegcd  16542  ncoprmlnprm  16765  setsstruct2  17211  efmnd2hash  18907  symg2hash  19409  pmtrdifellem2  19495  unitgrp  20383  isdrngd  20765  isdrngdOLD  20767  bcthlem5  25362  lgsmulsqcoprm  27387  noetalem2  27787  colinearalg  28925  axcontlem8  28986  cplgr3v  29452  2wlkdlem3  29947  umgr2adedgwlk  29965  elwwlks2  29986  clwwlkinwwlk  30059  3wlkdlem5  30182  3wlkdlem6  30184  3wlkdlem7  30185  3wlkdlem8  30186  numclwwlk1lem2foalem  30370  chirredlem2  32410  rexdiv  32908  bnj944  34952  bnj969  34960  nnssi2  36456  nnssi3  36457  isdrngo2  37965  leatb  39293  paddasslem9  39830  paddasslem10  39831  dvhvaddass  41099  expgrowthi  44352  elsetpreimafveq  47384  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  gpgusgralem  48011  nn0mnd  48095  2zrngasgrp  48162  2zrngmsgrp  48169  mapprop  48262  lincvalpr  48335  refdivmptf  48463  refdivmptfv  48467  itsclc0yqsollem2  48684
  Copyright terms: Public domain W3C validator