ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim12i GIF version

Theorem anim12i 336
Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
Hypotheses
Ref Expression
anim12i.1 (𝜑𝜓)
anim12i.2 (𝜒𝜃)
Assertion
Ref Expression
anim12i ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem anim12i
StepHypRef Expression
1 anim12i.1 . 2 (𝜑𝜓)
2 anim12i.2 . 2 (𝜒𝜃)
3 id 19 . 2 ((𝜓𝜃) → (𝜓𝜃))
41, 2, 3syl2an 287 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  anim12ci  337  anim1i  338  anim2i  339  hban  1511  sbimi  1722  spsbbi  1800  2exeu  2069  cgsex2g  2696  cgsex4g  2697  spc2egv  2749  spc2gv  2750  sseq2  3091  unssin  3285  uneqin  3297  undif3ss  3307  prneimg  3671  ssunieq  3739  iuneq1  3796  iuneq2  3799  copsex2t  4137  soeq2  4208  tpexg  4335  eldifpw  4368  iunpw  4371  peano5  4482  opbrop  4588  xpsspw  4621  coeq1  4666  coeq2  4667  cnveq  4683  dmeq  4709  sotri  4904  elxp4  4996  elxp5  4997  funun  5137  funtp  5146  imain  5175  2elresin  5204  funssxp  5262  fssres  5268  f1co  5310  foun  5354  resdif  5357  f1oco  5358  fvun1  5455  elfvmptrab1  5483  fvreseq  5492  ftpg  5572  f1o2ndf1  6093  spc2ed  6098  smores  6157  nnaord  6373  nnm00  6393  brecop  6487  eroveu  6488  ecopovtrn  6494  ecopovtrng  6497  th3qlem1  6499  th3q  6502  ixpeq2  6574  djuexb  6897  addcmpblnq  7143  mulcmpblnq  7144  mulclnq  7152  dmaddpq  7155  dmmulpq  7156  mulcanenq  7161  distrnqg  7163  ltdcnq  7173  ltexnqq  7184  enq0breq  7212  mulcmpblnq0  7220  mulcanenq0ec  7221  addnnnq0  7225  mulnnnq0  7226  mulclnq0  7228  nqpnq0nq  7229  nqnq0a  7230  nqnq0m  7231  distrnq0  7235  elinp  7250  genpml  7293  genpmu  7294  genprndl  7297  genprndu  7298  addnqprl  7305  addnqpru  7306  distrlem1prl  7358  distrlem1pru  7359  ltsopr  7372  cauappcvgprlemdisj  7427  caucvgprlemdisj  7450  caucvgprprlemdisj  7478  addcmpblnr  7515  addsrpr  7521  mulsrpr  7522  addclsr  7529  addasssrg  7532  0idsr  7543  1idsr  7544  00sr  7545  mulgt0sr  7554  axaddcl  7640  axmulcl  7642  axaddass  7648  axdistr  7650  cnegexlem3  7907  cnegex  7908  apirr  8334  recexaplem2  8380  zletric  9056  zlelttric  9057  qaddcl  9383  qmulcl  9385  qreccl  9390  iccss  9679  fzsubel  9795  elfz0add  9855  difelfznle  9867  2ffzeq  9873  fzonmapblen  9919  ubmelfzo  9932  ubmelm1fzo  9958  subfzo0  9974  qletric  9976  qlelttric  9977  adddivflid  10020  mulexp  10287  mulexpzap  10288  leexp1a  10303  faclbnd  10442  rexanuz  10715  sqabsadd  10782  sqabssub  10783  abs2dif  10833  rpmincl  10964  xrminrpcl  10998  fsum2dlemstep  11158  summodnegmod  11436  dvds2ln  11438  dvdsflip  11461  gcdsupex  11558  gcdsupcl  11559  gcdabs  11588  sqgcd  11629  lcmabs  11669  lcmgcdlem  11670  lcmgcd  11671  lcmgcdeq  11676  qredeq  11689  cncongr1  11696  cncongr2  11697  hashgcdlem  11814  tgcl  12144  uncld  12193  innei  12243  cnco  12301  txbas  12338  txbasval  12347  blin2  12512  qtopbasss  12601  bj-indind  13026
  Copyright terms: Public domain W3C validator