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 206  df-an 396

This theorem is referenced by:  sylan  579  vtocl2gf  3556  vtocl3gf  3557  vtocl2g  3558  vtocl3g  3559  vtoclegftOLD  3570  sbcthdv  3790  elinsn  4710  axprlem4  5420  swopolem  5594  wereu  5668  funssres  6591  dffv2  6987  fmptcof  7133  fnprb  7214  fntpb  7215  fliftfuns  7316  isorel  7328  oveqrspc2v  7441  caovclg  7607  caovcomg  7610  caovassg  7613  caovcang  7616  caovordig  7620  caovordg  7622  caovdig  7629  caovdirg  7632  peano5  7893  peano5OLD  7894  dmfexALT  7910  frpoins3xp3g  8140  fvmpocurryd  8270  qliftfuns  8814  nneneq  9225  nneneqOLD  9237  ttrcltr  9731  ttrclselem2  9741  frins3  9770  cfslb  10281  hsmexlem4  10444  axdc3lem2  10466  axdc4lem  10470  adderpq  10971  mulerpq  10972  ltordlem  11761  lble  12188  uz11  12869  xrsupsslem  13310  xrinfmsslem  13311  xrsupss  13312  xrinfmss  13313  fseqsupubi  13967  hashbclem  14435  ccatass  14562  swrdswrd  14679  swrdccatin1  14699  swrdccatin2  14703  cshwcsh2id  14803  wwlktovf  14931  isercolllem1  15635  caucvgb  15650  zsum  15688  fsum  15690  fsumf1o  15693  fsumcvg2  15697  isummulc2  15732  fsum2dlem  15740  fsumcom2  15744  fsumshftm  15751  fsum0diag2  15753  fsum00  15768  fsumrlim  15781  o1fsum  15783  isumshft  15809  clim2prod  15858  ntrivcvgfvn0  15869  zprod  15905  fprod  15909  fprodf1o  15914  prodss  15915  fprodser  15917  fprodcllemf  15926  fprodm1s  15938  fprodp1s  15939  fprodabs  15942  fprod2dlem  15948  fprodcom2  15952  fprodefsum  16063  mod2eq1n2dvds  16315  sumeven  16355  lcmfun  16607  pythagtriplem4  16779  pcmptdvds  16854  prslem  18281  posi  18300  dlatmjdi  18506  lidrididd  18621  grpidinv2  18945  ghmlin  19166  cntzmhm2  19284  dprdss  19977  dprd2d2  19992  srgrz  20138  srglz  20139  ringinvnz1ne0  20225  lmodlema  20737  islmodd  20738  lsscl  20815  lsslss  20834  lspdisjb  21003  rrgeq0i  21225  lsslinds  21752  assalem  21778  fvmptnn04if  22738  chfacfscmulgsum  22749  chfacfpmmulgsum  22753  ssnei2  23007  t1ficld  23218  t1sep2  23260  unconn  23320  1stcclb  23335  ptbasfi  23472  tx1stc  23541  qtoptop2  23590  r0sep  23639  ustincl  24099  ustdiag  24100  ustinvel  24101  ustexhalf  24102  psmet0  24201  psmettri2  24202  prdsdsf  24260  prdsxmet  24262  cncfi  24801  ovolfiniun  25417  mbfimaopnlem  25571  limciun  25810  dvcn  25838  dvmptfsum  25894  dvfsumle  25941  dvfsumleOLD  25942  dvfsumabs  25944  dvfsumlem3  25950  itgsubst  25971  fsumvma  27133  dchrelbasd  27159  dchrisumlem3  27411  sssslt1  27715  sssslt2  27716  madeval2  27767  elmade  27781  axcontlem9  28770  usgruspgrb  28983  uspgrloopvtxel  29317  umgr2v2evtxel  29323  clwwlknonex2lem2  29905  3spthd  29973  grpoass  30300  lnolin  30551  elnlfn  31725  strlem4  32051  hstrlem4  32059  atmd  32196  nn0min  32565  omndadd  32764  slmdlema  32888  qsxpid  33014  esumcvg  33641  measxun2  33765  sibfima  33894  bnj110  34425  bnj594  34479  bnj1491  34624  loop1cycl  34683  cvmcov  34809  mrsubcn  35065  dfon2lem5  35319  ifscgr  35576  nn0prpw  35743  neibastop2lem  35780  bj-restb  36509  poimirlem25  37053  poimirlem32  37060  mbfresfi  37074  totbndss  37185  ghomlinOLD  37296  rngodi  37312  rngodir  37313  rngoass  37314  rngohomadd  37377  rngohommul  37378  crngocom  37409  idladdcl  37427  idllmulcl  37428  idlrmulcl  37429  exlimddvf  37529  oposlem  38591  cvlexch1  38737  hlsuprexch  38791  lautle  39494  elrfirn2  42038  wepwsolem  42388  kelac1  42409  islssfg2  42417  lnmlssfg  42426  onov0suclim  42626  ovolval5lem3  45965  2elfz3nn0  46619  2elfz2melfz  46621  icceuelpartlem  46698  wtgoldbnnsum4prm  47065  bgoldbnnsum3prm  47067  bgoldbtbnd  47072  setrec2fun  48046