Theorem 3impia 1135

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 459	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1134	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mopick2  2662  ceqsalt  3483  3gencl  3493  vtoclgft  3515  rspc6v  3596  mob2  3672  moi  3675  reupick3  4274  disjne  4407  elpr2elpr  4823  disji2  5086  disji  5087  tz7.2  5634  sofld  6181  ordintdif  6417  funopg  6579  fvun1  6981  fvopab6  7033  fveqressseq  7084  fvcofneq  7098  fprg  7164  isores3  7347  ovmpt4g  7571  ovmpos  7572  ov2gf  7573  ofrval  7709  sorpssuni  7752  sorpssint  7753  poxp  8146  poseq  8181  suppss2  8224  frrlem12  8322  smoel  8375  smoord  8380  smogt  8382  oaass  8576  oewordi  8607  oeoalem  8612  oeoelem  8614  nnawordi  8637  nnaass  8638  naddssim  8702  qsel  8824  xpdom3  9101  onsdominel  9152  mapdom3  9175  sdomdomtrfi  9223  domsdomtrfi  9224  php  9229  onomeneq  9236  fisseneq  9261  fodomfir  9326  cantnflem1  9697  ttrclss  9728  cfslbn  10352  cfsmolem  10355  cfcoflem  10357  infpssrlem4  10391  fin23lem7  10401  fin23lem25  10409  isf34lem7  10464  hsmexlem2  10512  axcc3  10523  axdc4lem  10540  tskss  10850  gruss  10888  gruurn  10890  gruiun  10891  gruel  10895  gruen  10904  grudomon  10909  grothac  10922  axpre-sup  11261  axsup  11392  addn0nid  11743  letrp1  12168  p1le  12169  lemul1a  12178  infrelb  12309  nnadddir  12401  zextle  12779  zextlt  12780  btwnnz  12782  gtndiv  12783  uzind2  12799  fzind  12804  zsupss  13071  xrltne  13299  lemaxle  13332  qbtwnre  13336  qbtwnxr  13337  xlemul1a  13425  icogelb  13534  iccleub  13539  iccsplit  13623  uzsubsubfz  13687  elfz0fzfz0  13774  difelfznle  13783  fvffz0  13787  elfzo0le  13845  fzonmapblen  13850  fzofzim  13851  ceile  13996  modadd1  14055  muladdmodid  14060  modmul1  14074  modirr  14092  fsuppmapnn0fiub0  14143  expcl2lem  14223  expclzlem  14233  expnegz  14246  leexp2r  14324  bcval4  14458  bccmpl  14460  hashbnd  14487  hashunsnggt  14545  hashgt23el  14576  hashfundm  14594  elovmpowrd  14710  ccatval2  14730  ccatrcl1  14748  wrdl1s1  14770  ccat2s1fvw  14794  swrdsb0eq  14821  swrdccatin1  14882  pfxccatpfx2  14894  repswswrd  14943  cshwcsh2id  14987  sgn3da  15263  absexpz  15481  climbdd  15848  iseraltlem2  15859  binomfallfac  16216  dvdsle  16489  divalgb  16583  ndvdssub  16588  dvdsgcd  16726  dfgcd2  16728  rplpwr  16741  nn0rppwr  16744  nn0expgcd  16747  lcmgcdlem  16790  lcmfunsn  16828  coprmdvds1  16836  qredeq  16841  2mulprm  16877  prmdvdsexpr  16902  nnnn0modprm0  16993  prm23ge5  17002  pcexp  17046  difsqpwdvds  17074  prmpwdvds  17091  ramcl  17216  cshwshashlem3  17284  cshwrepswhash1  17289  elrestr  17608  mreintcl  17774  mremre  17783  mrieqv2d  17822  initoeu2lem1  18198  funcestrcsetclem9  18331  funcsetcestrclem9  18346  prstr  18482  drsdirfi  18488  latnlej  18639  latnlej2  18642  acsdrsel  18726  acsdrscl  18729  mrelatglb  18743  mrelatlub  18745  isnmgm  18829  grpasscan1  19221  grpinvnz  19229  mulgneg2  19327  gsmsymgrfix  19651  f1omvdco2  19671  symggen  19693  odcl2  19788  odhash3  19799  lsmss1  19888  lsmss2  19890  efgred  19971  efgcpbl  19979  ablfacrp  20291  ablfac1eu  20298  ablfaclem3  20312  omndadd  20351  ogrpaddlt  20361  dvdsrmul1  20608  dvdsunit  20618  irredmul  20668  c0snmgmhm  20701  lmodlema  21149  psgnodpmr  21905  phlssphl  21974  lindsss  22139  lindfmm  22142  ply1scln0  22619  dmatelnd  22820  mdetdiaglem  22922  mdet0  22930  mdetunilem7  22942  slesolinv  23007  cramerimplem3  23012  cpmatpmat  23037  m2cpminvid2lem  23081  chfacfscmul0  23185  chfacfpmmul0  23189  riinopn  23235  clsndisj  23402  cnpf2  23577  hausnei2  23680  cmpcov  23716  cmpfii  23736  unconn  23756  t1connperf  23763  nrmr0reg  24077  fbfinnfr  24169  filuni  24213  alexsubALT  24379  tmdgsum  24423  cuspcvg  24628  mopni  24820  isngp4  24940  metdsre  25182  iimulcl  25267  phtpc01  25326  clmmulg  25431  cfilucfil4  25651  bcthlem5  25658  bcth  25659  bcth3  25661  itg1le  26043  itg2le  26069  bddmulibl  26168  bddiblnc  26171  dvnres  26260  cpnord  26264  dvnfre  26281  deg1ge  26425  dgr1term  26588  aaliou3lem2  26679  sincosq1lem  26835  cxpge0  27020  cxpmul2  27026  logrec  27100  logbgcd1irr  27131  sqfpc  27473  bcmono  27613  gausslemma2dlem1a  27701  gausslemma2dlem2  27703  gausslemma2dlem4  27705  2lgsoddprmlem3  27750  pntrmax  27900  qabvexp  27962  ostth2lem2  27970  fltoprmlem2  28003  nosepon  28031  nolesgn2o  28037  nogesgn1o  28039  nosepnelem  28045  nosepne  28046  nosepdmlem  28049  nosepdm  28050  nodenselem8  28057  noresle  28063  noetasuplem4  28102  noetainflem4  28106  cutbdaylt  28193  eqcuts3  28199  addsuniflem  28396  sltmuls1  28542  precsexlem6  28607  precsexlem7  28608  precsexlem11  28612  ltonold  28656  onnolt  28661  n0fincut  28750  oldfib  28772  expadds  28830  ax5seglem4  29519  axeuclidlem  29549  uhgredgrnv  29717  usgredg4  29807  nbuhgr2vtx1edgblem  29941  vtxduhgr0e  30068  vtxduhgr0nedg  30082  rusgrpropnb  30173  uspgr2wlkeqi  30237  redwlklem  30259  lfgrwlkprop  30279  2pthnloop  30326  spthonepeq  30347  pthdlem2lem  30362  crctcshwlkn0lem3  30410  crctcshwlkn0lem5  30412  crctcshwlkn0lem7  30414  crctcshwlkn0  30419  wlkiswwlks1  30465  wlkiswwlks2  30473  wlkiswwlksupgr2  30475  wwlksnext  30491  wwlksnextproplem2  30508  wspthsnonn0vne  30515  2pthon3v  30541  rusgrnumwwlk  30576  erclwwlkeqlen  30619  erclwwlksym  30621  erclwwlktr  30622  erclwwlkneqlen  30668  erclwwlknsym  30670  erclwwlkntr  30671  uhgr3cyclex  30792  upgreupthseg  30819  eupth2lem3lem4  30841  eucrctshift  30853  4cycl2vnunb  30900  nvs  31274  nvtri  31281  nmlno0  31406  nmlnoubi  31407  ubth  31484  hlipgt0  31525  ocnel  31909  elspansn2  32178  elspansn3  32183  normcan  32187  pjoml2  32222  lecm  32228  osum  32256  nmbdfnlb  32661  leopmul  32745  hstpyth  32840  cvnbtwn  32897  ssmd1  32922  ssmd2  32923  ssdmd1  32924  ssdmd2  32925  cvmd  32947  cvdmd  32948  superpos  32965  disji2f  33222  disjif  33223  disjif2  33226  preiman0  33354  padct  33361  ffs2  33369  bcm1n  33437  s2f1  33560  archiabl  33809  slmdlema  33814  lbslsat  34298  eulerpartlemb  35050  nelscottrankgt  35807  acwer1prc  35820  onprcf1acwevdlem1  35968  fisshasheq  35983  cvmsdisj  36125  cvmlift2lem12  36169  satfrel  36222  satfrnmapom  36225  fmlasuc  36241  satffun  36264  satef  36271  sategoelfv  36275  lineintmo  37018  nmuladdss  37058  nn0prpwlem  37206  nn0prpw  37207  neibastop2lem  37244  tr0elw  37368  lindsadd  38645  areacirc  38740  incsequz  38791  mettrifi  38800  ismtybnd  38850  heiborlem1  38854  rngoisocnv  39024  risci  39030  eqvrelqsel  39741  lfl1  40236  lkrlsp2  40269  omlfh3N  40425  cvrnbtwn  40437  cvrnbtwn2  40441  cvrnbtwn4  40445  cvlexch3  40498  cvlexch4N  40499  cvlatexchb1  40500  2llnne2N  40574  atcvrj0  40594  cvrat2  40595  ps-1  40643  3atlem5  40653  islln2a  40683  lplnriaN  40716  lplnribN  40717  llncvrlpln2  40723  lplncvrlvol2  40781  psubatN  40921  pmapglb2N  40937  pmapglb2xN  40938  2llnma1b  40952  paddasslem17  41002  pmod2iN  41015  pmodl42N  41017  hlmod1i  41022  atmod1i1  41023  atmod1i2  41025  llnmod1i2  41026  pclcmpatN  41067  osumcllem8N  41129  pexmidlem3N  41138  pl42lem4N  41148  4atexlem7  41241  ltrnnid  41302  cdlemc4  41360  cdleme32a  41607  cdlemeg46gfre  41698  cdlemf2  41728  cdlemg4c  41778  trlcoat  41889  tendovalco  41931  tendoeq2  41940  cdlemk36  42079  diael  42209  diatrl  42210  dicelval1stN  42354  dicelval2nd  42355  dihlspsnat  42499  dochkr1  42644  lcfrlem9  42716  mapdh8e  42950  hdmapval0  42999  hgmapval0  43058  dvdsexpnn0  43495  incssnn0  43831  pell14qrexpcl  43983  pell14qrgap  43991  congadd  44082  acongsym  44092  acongtr  44094  dvdsacongtr  44100  jm2.19lem3  44107  jm2.19lem4  44108  jm2.26lem3  44117  onexlimgt  44354  nadd2rabex  44497  ismnushort  45394  bi13impia  45580  3impcombi  45907  ioogtlb  46615  iocgtlb  46622  iocleub  46623  icoltub  46628  iooltub  46630  limclner  46769  limsupre3lem  46850  climuzlem  46861  fsupdm  47960  finfdm  47964  elfzelfzlble  48499  subsubelfzo0  48505  m1modnep2mod  48536  m1modmmod  48542  modlt0b  48547  mod2addne  48548  iccpartigtl  48613  sqrtpwpw2p  48731  fmtnoprmfac1lem  48757  fmtno4prmfac  48765  evenltle  48923  even3prm2  48925  wtgoldbnnsum4prm  49008  bgoldbnnsum3prm  49010  bgoldbtbndlem1  49011  bgoldbtbndlem3  49013  bgoldbtbndlem4  49014  bgoldbtbnd  49015  uhgrimisgrgriclem  49136  isubgr3stgrlem7  49178  clnbgr3stgrgrlic  49226  gpgedg2iv  49273  pgnbgreunbgrlem3  49324  pgnbgreunbgrlem6  49330  upgrwlkupwlk  49346  funcringcsetcALTV2lem9  49503  funcringcsetclem9ALTV  49526  lincscmcl  49652  lindslinindimp2lem4  49681  lincresunit2  49698  lincresunit3  49701  elfzolborelfzop1  49739  rege1logbzge0  49779  fllog2  49788  dignn0ldlem  49822  rrx2pnecoorneor  49936  rrx2plord2  49943  rrx2linest  49962  itscnhlinecirc02p  50005  ipolub  50210  ipoglb  50213