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  2800  vtocl3gf  2801  vtoclegft  2810  sbcthdv  2978  disji2  3997  exmid1stab  4209  swopolem  4306  funssres  5259  fvmptssdm  5601  fmptcof  5684  fliftfuns  5799  isorel  5809  oveqrspc2v  5902  caovclg  6027  caovcomg  6030  caovassg  6033  caovcang  6036  caovordig  6040  caovordg  6042  caovdig  6049  caovdirg  6052  qliftfuns  6619  nneneq  6857  supmoti  6992  exmidonfinlem  7192  recexprlemopl  7624  recexprlemopu  7626  cauappcvgprlemladdrl  7656  caucvgsrlemcl  7788  caucvgsrlemfv  7790  caucvgsr  7801  suplocsrlempr  7806  ltordlem  8439  lble  8904  uz11  9550  seq3caopr3  10481  climcaucn  11359  sumdc  11366  fsum3  11395  fsumf1o  11398  fsum3cvg2  11402  isummulc2  11434  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fisum0diag2  11455  fsum00  11470  isumshft  11498  clim2prod  11547  prodmodclem2  11585  zproddc  11587  fprodseq  11591  fprodf1o  11596  prodssdc  11597  fprodm1s  11609  fprodp1s  11610  fprodcllemf  11621  fprodabs  11624  fprod2dlemstep  11630  fprodcom2fi  11634  dvdsprm  12137  pythagtriplem4  12268  pcmptdvds  12343  lidrididd  12801  grpidinv2  12928  srgrz  13167  srglz  13168  ringinvnz1ne0  13226  lmodlema  13382  islmodd  13383  ssnei2  13660  psmet0  13830  psmettri2  13831  cncfi  14068  dvcn  14167  nninfsellemdc  14762