Theorem mpan9 506

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 34	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 407	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  sylan  581  vtocl2gf  3529  vtocl3gf  3530  vtocl2g  3531  vtocl3g  3532  sbcthdv  3758  elinsn  4669  axprlem4OLD  5376  swopolem  5550  wereu  5628  funssres  6544  dffv2  6937  fmptcof  7085  fnprb  7164  fntpb  7165  fliftfuns  7270  isorel  7282  oveqrspc2v  7395  caovclg  7560  caovcomg  7563  caovassg  7566  caovcang  7569  caovordig  7573  caovordg  7575  caovdig  7582  caovdirg  7585  caofidlcan  7670  peano5  7845  dmfexALT  7860  frpoins3xp3g  8093  fvmpocurryd  8223  qliftfuns  8753  nneneq  9142  ttrcltr  9637  ttrclselem2  9647  frins3  9679  cfslb  10188  hsmexlem4  10351  axdc3lem2  10373  axdc4lem  10377  adderpq  10879  mulerpq  10880  ltordlem  11674  lble  12106  uz11  12788  xrsupsslem  13234  xrinfmsslem  13235  xrsupss  13236  xrinfmss  13237  fseqsupubi  13913  hashbclem  14387  ccatass  14524  swrdswrd  14640  swrdccatin1  14660  swrdccatin2  14664  cshwcsh2id  14763  wwlktovf  14891  isercolllem1  15600  caucvgb  15615  zsum  15653  fsum  15655  fsumf1o  15658  fsumcvg2  15662  isummulc2  15697  fsum2dlem  15705  fsumcom2  15709  fsumshftm  15716  fsum0diag2  15718  fsum00  15733  fsumrlim  15746  o1fsum  15748  isumshft  15774  clim2prod  15823  ntrivcvgfvn0  15834  zprod  15872  fprod  15876  fprodf1o  15881  prodss  15882  fprodser  15884  fprodcllemf  15893  fprodm1s  15905  fprodp1s  15906  fprodabs  15909  fprod2dlem  15915  fprodcom2  15919  fprodefsum  16030  mod2eq1n2dvds  16286  sumeven  16326  lcmfun  16584  pythagtriplem4  16759  pcmptdvds  16834  prslem  18232  posi  18252  dlatmjdi  18458  lidrididd  18607  grpidinv2  18939  ghmlin  19162  cntzmhm2  19283  dprdss  19972  dprd2d2  19987  omndadd  20069  srgrz  20154  srglz  20155  ringinvnz1ne0  20247  rrgeq0i  20644  lmodlema  20828  islmodd  20829  lsscl  20905  lsslss  20924  lspdisjb  21093  lsslinds  21798  assalem  21824  fvmptnn04if  22805  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  ssnei2  23072  t1ficld  23283  t1sep2  23325  unconn  23385  1stcclb  23400  ptbasfi  23537  tx1stc  23606  qtoptop2  23655  r0sep  23704  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  psmet0  24264  psmettri2  24265  prdsdsf  24323  prdsxmet  24325  cncfi  24855  ovolfiniun  25470  mbfimaopnlem  25624  limciun  25863  dvcn  25891  dvmptfsum  25947  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem3  26003  itgsubst  26024  fsumvma  27192  dchrelbasd  27218  dchrisumlem3  27470  ssslts1  27781  ssslts2  27782  madeval2  27841  elmade  27865  axcontlem9  29057  usgruspgrb  29268  uspgrloopvtxel  29602  umgr2v2evtxel  29608  clwwlknonex2lem2  30195  3spthd  30263  grpoass  30591  lnolin  30842  elnlfn  32016  strlem4  32342  hstrlem4  32350  atmd  32487  nn0min  32912  slmdlema  33297  qsxpid  33455  esumcvg  34264  measxun2  34388  sibfima  34516  bnj110  35034  bnj594  35088  bnj1491  35233  loop1cycl  35353  cvmcov  35479  mrsubcn  35735  dfon2lem5  36001  ifscgr  36260  nn0prpw  36539  neibastop2lem  36576  bj-restb  37347  poimirlem25  37896  poimirlem32  37903  mbfresfi  37917  totbndss  38028  ghomlinOLD  38139  rngodi  38155  rngodir  38156  rngoass  38157  rngohomadd  38220  rngohommul  38221  crngocom  38252  idladdcl  38270  idllmulcl  38271  idlrmulcl  38272  exlimddvf  38372  oposlem  39558  cvlexch1  39704  hlsuprexch  39757  lautle  40460  elrfirn2  43053  wepwsolem  43399  kelac1  43420  islssfg2  43428  lnmlssfg  43437  onov0suclim  43631  relprel  45307  ovolval5lem3  47012  2elfz3nn0  47676  2elfz2melfz  47678  icceuelpartlem  47795  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbnd  48169  gpgedg2iv  48427  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  oppcendc  49377  setrec2fun  50051