Theorem mpan9 281

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 32	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 125	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  sylan  283  vtocl2gf  2877  vtocl3gf  2878  vtoclegft  2889  sbcthdv  3057  disji2  4101  exmid1stab  4321  swopolem  4426  funssres  5395  fvmptssdm  5762  fmptcof  5844  fliftfuns  5971  isorel  5981  oveqrspc2v  6077  caovclg  6207  caovcomg  6210  caovassg  6213  caovcang  6216  caovordig  6220  caovordg  6222  caovdig  6229  caovdirg  6232  qliftfuns  6853  nneneq  7111  supmoti  7284  exmidonfinlem  7496  recexprlemopl  7940  recexprlemopu  7942  cauappcvgprlemladdrl  7972  caucvgsrlemcl  8104  caucvgsrlemfv  8106  caucvgsr  8117  suplocsrlempr  8122  ltordlem  8756  lble  9221  uz11  9877  seq3caopr3  10853  hashfibclem  11206  ccatass  11296  swrdswrd  11397  swrdccatin1  11417  swrdccatin2  11421  climcaucn  12036  sumdc  12043  fsum3  12073  fsumf1o  12076  fsum3cvg2  12080  isummulc2  12112  fsum2dlemstep  12120  fisumcom2  12124  fsumshftm  12131  fisum0diag2  12133  fsum00  12148  isumshft  12176  clim2prod  12225  prodmodclem2  12263  zproddc  12265  fprodseq  12269  fprodf1o  12274  prodssdc  12275  fprodm1s  12287  fprodp1s  12288  fprodcllemf  12299  fprodabs  12302  fprod2dlemstep  12308  fprodcom2fi  12312  dvdsprm  12834  pythagtriplem4  12966  pcmptdvds  13043  lidrididd  13595  grpidinv2  13771  ghmlin  13965  srgrz  14128  srglz  14129  ringinvnz1ne0  14193  rrgeq0i  14409  lmodlema  14440  islmodd  14441  lsslss  14529  ssnei2  15022  psmet0  15192  psmettri2  15193  cncfi  15443  dvcn  15565  dvmptfsum  15590  usgruspgrben  16181  wlk1walkdom  16354  clwwlknonex2lem2  16433  nninfsellemdc  16788