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

Theorem anim12i 331
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 283 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  anim12ci  332  anim1i  333  anim2i  334  hban  1480  sbimi  1688  spsbbi  1766  2exeu  2034  cgsex2g  2636  cgsex4g  2637  spc2egv  2688  spc2gv  2689  sseq2  3022  unssin  3210  uneqin  3222  undif3ss  3232  prneimg  3574  ssunieq  3642  iuneq1  3699  iuneq2  3702  copsex2t  4008  soeq2  4079  tpexg  4205  eldifpw  4234  iunpw  4237  peano5  4347  opbrop  4445  xpsspw  4478  coeq1  4521  coeq2  4522  cnveq  4537  dmeq  4563  sotri  4750  elxp4  4838  elxp5  4839  funun  4974  funtp  4983  imain  5012  2elresin  5041  funssxp  5091  fssres  5097  f1co  5132  foun  5176  resdif  5179  f1oco  5180  fvun1  5271  fvreseq  5303  ftpg  5379  f1o2ndf1  5880  spc2ed  5885  smores  5941  nnaord  6148  nnm00  6168  brecop  6262  eroveu  6263  ecopovtrn  6269  ecopovtrng  6272  th3qlem1  6274  th3q  6277  addcmpblnq  6619  mulcmpblnq  6620  mulclnq  6628  dmaddpq  6631  dmmulpq  6632  mulcanenq  6637  distrnqg  6639  ltdcnq  6649  ltexnqq  6660  enq0breq  6688  mulcmpblnq0  6696  mulcanenq0ec  6697  addnnnq0  6701  mulnnnq0  6702  mulclnq0  6704  nqpnq0nq  6705  nqnq0a  6706  nqnq0m  6707  distrnq0  6711  elinp  6726  genpml  6769  genpmu  6770  genprndl  6773  genprndu  6774  addnqprl  6781  addnqpru  6782  distrlem1prl  6834  distrlem1pru  6835  ltsopr  6848  cauappcvgprlemdisj  6903  caucvgprlemdisj  6926  caucvgprprlemdisj  6954  addcmpblnr  6978  addsrpr  6984  mulsrpr  6985  addclsr  6992  addasssrg  6995  0idsr  7006  1idsr  7007  00sr  7008  mulgt0sr  7016  axaddcl  7094  axmulcl  7096  axaddass  7100  axdistr  7102  cnegexlem3  7352  cnegex  7353  apirr  7772  recexaplem2  7809  zletric  8476  zlelttric  8477  qaddcl  8801  qmulcl  8803  qreccl  8808  iccss  9040  fzsubel  9154  elfz0add  9211  difelfznle  9223  2ffzeq  9228  fzonmapblen  9273  ubmelfzo  9286  ubmelm1fzo  9312  subfzo0  9328  qletric  9330  qlelttric  9331  adddivflid  9374  mulexp  9612  mulexpzap  9613  leexp1a  9628  faclbnd  9765  rexanuz  10012  sqabsadd  10079  sqabssub  10080  abs2dif  10130  summodnegmod  10371  dvds2ln  10373  dvdsflip  10396  gcdsupex  10493  gcdsupcl  10494  gcdabs  10523  sqgcd  10562  lcmabs  10602  lcmgcdlem  10603  lcmgcd  10604  lcmgcdeq  10609  qredeq  10622  cncongr1  10629  cncongr2  10630  bj-indind  10885
  Copyright terms: Public domain W3C validator